es:ES, A:Type, l:IdLnk, tg:Id, ds:x:Id fp Type,
conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
(k:Knd. (k  dom(conds))  (hasloc(k;source(l))))
 (e:E. (kind(e) = rcv(l,tg)  Knd)  (valtype(e) r A))
 (k:Knd.
 (k  dom(conds))
  k(v:conds(k).1) sends on l [tg:A, p.let s,v = p in (conds(k).2)(s,v) <state, v>]?[])
 only events in fpf-domain(conds) send on l with tg
 glues(es;
 glues(A;
 glues((e.sender(e));
 glues((e.outl((conds(kind(e)).2)((state when e),val(e))));
 glues(es-triggers(es;source(l);ds;conds);
 glues(es-in-port(es;l;tg)) 

latex

Definitions

ES, t  T, f(a), EState(T), Id, , x:AB(x), x:A. B(x), pred!(e;e'), SWellFounded(R(x;y)), Unit, Void, x:A.B(x), Top, S  T, left + right, Type, suptype(S; T), first(e), b, A, loc(e), <a, b>, s = t, P  Q, constant_function(f;A;B), IdLnk, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Msg(M), type List, kind(e), EOrderAxioms(E; pred?; info), EqDecider(T), (x  l), {x:A| B(x)} , Atom$n, State(ds), a:A fp B(a), x.A(x), source(l), hasloc(k;i), KindDeq, x  dom(f), valtype(e), rcv(l,tg), kind(e), E, if b then t else f fi , f(x), t.1, t.2, let x,y = A in B(x;y), k(v:B) sends on l [tg:T, f <state, v>]?[], , fpf-domain(f), only events in L send on l with tg, es-triggers(es;i;ds;conds), glues(es; B; g; f; Ia; Ib), a = b, P  Q, P  Q, {T}, loc(e), state@i, IdDeq, f(x)?z, False, vartype(i;x), A c B, sender(e), lnk(e), isrcv(e), Dec(P), True, P  Q, b, es-in-port(es;l;tg), (I|p), val(e), (state when e), outl(x), Inj(A;B;f), f is Q-R-pre-preserving on P, Q = f== P, g glues Ia:Qa f Ib:Rb, e  X, inr x , inl x , ff, product-deq(A;B;a;b), case b of inl(x) => s(x) | inr(y) => t(y), locl(a), SQType(T), s ~ t, T, destination(l), tt, acttype(e), rcvtype(e), AbsInterface(A), E(X), @i discrete ds, e loc e' , a < b, SqStable(P)

Lemmas

member-fpf-domain, Knd sq, sq stable from decidable, es-is-interface-in-port, es-kind-rcv, es-is-interface-triggers, Q-R-glues-trivial-restrict, es-le wf, es-triggers wf, outl wf, es-state-when wf, es-state-subtype2, es-dds wf, subtype rel dep function, subtype rel self, es-val wf, es-is-interface wf, es-E-interface wf, es-in-port wf, es-rcvtype wf, es-acttype wf, locl wf, btrue wf, bfalse wf, squash wf, ldst wf, es-isrcv-loc, Id sq, IdLnk sq, es-loc-pred, member-fpf-dom, sender-glues-triggers2, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, es-isrcv wf, decidable false, decidable cand, false wf, true wf, decidable equal IdLnk, es-lnk wf, decidable and, decidable equal Id, decidable assert, es-sender wf, es-state-subtype-iff, es-state-subtype, es-vartype wf, fpf-cap wf, id-deq wf, es-loc wf, all functionality wrt iff, implies functionality wrt iff, assert-eq-knd, eq knd wf, subtype rel wf, sframe-p wf, fpf-domain wf, conditional-send-p wf, pi2 wf, pi1 wf, fpf-ap wf, es-E wf, es-kind wf, rcv wf, es-valtype wf, fpf-dom wf, Kind-deq wf, hasloc wf, lsrc wf, fpf-trivial-subtype-top, decl-state wf, l member wf, deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf, event system wf